Step of Proof: top_wf
9,38
postcript
pdf
Inference at
*
I
of proof for Lemma
top
wf
:
Top
Type
latex
by Unfold `top` 0
latex
1
:
1:
(
x
:!Void().!Void())
Type
.
Definitions
Top
origin
Top 
Type
by Unfold `top` 0
1:
1: (
x:!Void().!Void()) Type
. Top Type
by Unfold `top` 0
1:
1: (x:!Void().!Void()) Type
.